NoTerminationCheckPositivity.agda:20,1-21,14
E is not strictly positive, because it occurs
in the 4th argument of M.F
in the type of the constructor e
in the definition of E.
